\begin{tabbing}
$\forall$\=$E$, $X_{1}$, $X_{2}$:Type, ${\it dE}$:EqDecider($E$), ${\it dL}$:EqDecider(IdLnk), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)),
\\[0ex]$p$:(\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]$\forall$${\it e''}$:$E$.
\\[0ex]rcv?(${\it e''}$)
\\[0ex]$\Rightarrow$ sender(${\it e''}$) $=$ $e$
\\[0ex]$\Rightarrow$ link(${\it e''}$) $=$ $l$
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\vee$ ${\it e''}$ $<$ ${\it e'}$ \& loc(${\it e'}$) $=$ destination($l$) $\in$ Id).
\-\-\\[0ex]SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ loc(pred($e$)) $=$ loc($e$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:$E$. loc($e$) $=$ loc(${\it e'}$) $\in$ Id $\Rightarrow$ ${\it pred?}$($e$) $=$ ${\it pred?}$(${\it e'}$) $\Rightarrow$ $e$ $=$ ${\it e'}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$r$:$E$.\+
\\[0ex]rcv?($r$)
\\[0ex]$\Rightarrow$ index(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;$p$;$r$) $\in$ $\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$receives(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;$p$;sender($r$);link($r$))$\parallel$}}$)
\-
\end{tabbing}